$\forall$$T$,$X$:Type, ${\it eq}$:EqDecider($X$), $f$,$g$:fpf($X$; $x$.Type), $x$:$X$.
\\[0ex]fpf{-}sub($X$; $x$.Type; ${\it eq}$; $g$; $f$) $\Rightarrow$ subtype\_rel(fpf{-}cap($f$; ${\it eq}$; $x$; $T$); fpf{-}cap($g$; ${\it eq}$; $x$; top))